1  /-
  2  Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Zhouhang Zhou
  5  -/
  6  
  7  import algebra.ordered_field
src         └───────────────────┘
  8  import tactic.linarith tactic.ring
src         └─────────────┘ └─────────┘
  9  
 10  /-!
 11  # Quadratic discriminants and roots of a quadratic
 12  
 13  This file defines the discriminant of a quadratic and gives the solution to a quadratic equation.
 14  
 15  ## Main definition
 16  
 17  The discriminant of a quadratic `a*x*x + b*x + c` is `b*b - 4*a*c`.
 18  
 19  ## Main statements
 20  • Roots of a quadratic can be written as `(-b + s) / (2 * a)` or `(-b - s) / (2 * a)`,
 21    where `s` is the square root of the discriminant.
 22  • If the discriminant has no square root, then the corresponding quadratic has no root.
 23  • If a quadratic is always non-negative, then its discriminant is non-positive.
 24  
 25  ## Tags
 26  
 27  polynomial, quadratic, discriminant, root
 28  -/
 29  
 30  variables {α : Type*}
 31  
 32  section lemmas
 33  
 34  variables [linear_ordered_field α] {a b c : α}
id              └──────────────────┘
src             └──────────────────┘
typ             └──────────────────┘
 35  
 36  lemma exists_le_mul_self : ∀ a : α, ∃ x : α, a ≤ x * x :=
id                                                
src                                                  
typ                                               
 37  begin
st   └─────
 38    assume a, cases le_total 1 a with ha ha,
id                     └──────┘   
src    └──────┘  └────┘└──────┘└─┘ └─────────┘
typ    └──────┘  └────┘└──────┘└─┘└─────────┘
doc    └──────┘  └────┘        └─┘ └─────────┘
txt    └──────┘  └────┘        └─┘ └─────────┘
par    └──────┘  └────┘        └─┘ └─────────┘
pid    └──────┘               └─┘ └─────────┘
st   ─────────┘└─────────────────────────────┘└─
 39    { use a, exact le_mul_of_ge_one_left (by linarith) ha },
id                   └───────────────────┘               └┘
src      └──┘   └────┘└───────────────────┘   └──────┘└┘  
typ      └──┘  └────┘└───────────────────┘   └──────┘└┘└┘
doc      └──┘   └────┘                        └──────┘└┘  
txt      └──┘   └────┘                        └──────┘└┘  
par      └──┘   └────┘                        └──────┘└┘  
pid                                         └─────────┘  
st   ───┘└───┘└───────────────────────────────┘└───────┘└───┘└┘
 40    { use 1, linarith }
src      └───┘  └───────┘
typ      └───┘  └───────┘
doc      └───┘  └───────┘
txt      └───┘  └───────┘
par      └───┘  └───────┘
pid                   
st   ────────┘└─────────┘└─
 41  end
st   ──┘
 42  
 43  lemma exists_lt_mul_self : ∀ a : α, ∃ x : α, a < x * x :=
id                                                
src                                                  
typ                                               
 44  begin
st   └─────
 45    assume a, rcases (exists_le_mul_self a) with ⟨x, hx⟩,
id                       └────────────────┘ 
src    └──────┘  └─────┘ └────────────────┘ └────────────┘
typ    └──────┘  └─────┘ └────────────────┘└────────────┘
doc    └──────┘  └─────┘                    └────────────┘
txt    └──────┘  └─────┘                    └────────────┘
par    └──────┘  └─────┘                    └────────────┘
pid    └──────┘                            └────────────┘
st   ─────────┘└──────────────────────────────────────────┘└─
 46    cases le_total 0 x with hx' hx',
id           └──────┘   
src    └────┘└──────┘└─┘ └───────────┘
typ    └────┘└──────┘└─┘└───────────┘
doc    └────┘        └─┘ └───────────┘
txt    └────┘        └─┘ └───────────┘
par    └────┘        └─┘ └───────────┘
pid                 └─┘ └───────────┘
st   ────────────────────────────────┘└─
 47    { use (x + 1),
id             
src      └──┘  └─┘
typ      └──┘ └─┘
doc      └──┘   └─┘
txt      └──┘   └─┘
par      └──┘   └─┘
pid            └─┘
st   ───┘└─────────┘└─
 48      have : (x+1)*(x+1) = x*x + 2*x + 1, ring,
id                                  
src      └─────┘   └┘   └─┘    └┘   └┘  └──┘
typ      └─────┘   └┘   └─┘    └┘  └┘  └──┘
doc      └─────┘   └┘    └─┘     └┘   └┘  └──┘
txt      └─────┘   └┘    └─┘     └┘   └┘  └──┘
par      └─────┘   └┘    └─┘     └┘   └┘  └──┘
pid      └───┘└┘   └┘    └─┘     └┘   
st   ─────────────────────────────────────┘└────┘└─
 49      exact lt_of_le_of_lt hx (by rw this; linarith) },
id             └────────────┘ └┘        └──┘
src      └────┘└────────────┘     └─┘    └┘└──────┘└┘
typ      └────┘└────────────┘└┘   └─┘└──┘└┘└──────┘└┘
doc      └────┘                   └─┘    └┘└──────┘└┘
txt      └────┘                   └─┘    └┘└──────┘└┘
par      └────┘                   └─┘    └┘└──────┘└┘
pid                              └──┘    └─────────┘
st   ──────────────────────────────┘└────────────────┘└┘└┘
 50    { use (x - 1),
id             
src      └──┘  └─┘
typ      └──┘ └─┘
doc      └──┘   └─┘
txt      └──┘   └─┘
par      └──┘   └─┘
pid            └─┘
st   ──────────────┘└─
 51      have : (x-1)*(x-1) = x*x - 2*x + 1, ring,
id                                    
src      └─────┘   └┘    └─┘     └┘   └┘  └──┘
typ      └─────┘   └┘    └─┘     └┘  └┘  └──┘
doc      └─────┘   └┘    └─┘     └┘   └┘  └──┘
txt      └─────┘   └┘    └─┘     └┘   └┘  └──┘
par      └─────┘   └┘    └─┘     └┘   └┘  └──┘
pid      └───┘└┘   └┘    └─┘     └┘   
st   ─────────────────────────────────────┘└────┘└─
 52      exact lt_of_le_of_lt hx (by rw this; linarith) }
id             └────────────┘ └┘        └──┘
src      └────┘└────────────┘     └─┘    └┘└──────┘└┘
typ      └────┘└────────────┘└┘   └─┘└──┘└┘└──────┘└┘
doc      └────┘                   └─┘    └┘└──────┘└┘
txt      └────┘                   └─┘    └┘└──────┘└┘
par      └────┘                   └─┘    └┘└──────┘└┘
pid                              └──┘    └─────────┘
st   ──────────────────────────────┘└────────────────┘└┘└─
 53  end
st   ──┘
 54  
 55  end lemmas
 56  
 57  variables [linear_ordered_field α] {a b c x : α}
id              └──────────────────┘
src             └──────────────────┘
typ             └──────────────────┘
 58  
 59  /-- Discriminant of a quadratic -/
 60  def discrim [ring α] (a b c : α) : α := b^2 - 4 * a * c
id                └──┘                            
src               └──┘                                
typ               └──┘                            
 61  
 62  /--
 63  A quadratic has roots if and only if its discriminant equals some square.
 64  -/
 65  lemma quadratic_eq_zero_iff_discrim_eq_square (ha : a ≠ 0) :
id                                                        
src                                                        
typ                                                       
 66    ∀ x : α, a * x * x + b * x + c = 0 ↔  discrim a b c = (2 * a * x + b)^2 :=
id                             └─────┘              
src                                   └─────┘                    
typ                            └─────┘              
doc                                          └─────┘
 67  assume x, iff.intro
id            └───────┘
src            └───────┘
typ           └───────┘
 68    (assume h, calc
id             
typ            
 69        discrim a b c = 4*a*(a*x*x + b*x + c) + b*b - 4*a*c : by rw [h, discrim]; ring
id         └─────┘                              └─────┘
src        └─────┘                                      └──┘ └┘└─────┘  └────
typ        └─────┘                        └──┘└┘└─────┘  └────
doc        └─────┘                                                  └──┘ └┘└─────┘  └────
txt                                                                 └──┘ └┘         └────
par                                                                 └──┘ └┘         └────
pid                                                                   └┘ └┘             
st                                                                 └────┘└───────┘└──────
 70        ... = (2*a*x + b)^2 : by ring)
id                    
src  ─────┘                     └──┘
typ  ─────┘                  └──┘
doc  ─────┘                         └──┘
txt  ─────┘                         └──┘
par  ─────┘                         └──┘
pid  ─────┘
st   ─────┘                        └───┘
 71    (assume h,
id             
typ            
 72      have ha : 2*2*a ≠ 0 := mul_ne_zero (mul_ne_zero two_ne_zero two_ne_zero) ha,
id                          └─────────┘  └─────────┘ └─────────┘ └─────────┘  └┘
src                          └─────────┘  └─────────┘ └─────────┘ └─────────┘
typ                         └─────────┘  └─────────┘ └─────────┘ └─────────┘  └┘
 73      eq_of_mul_eq_mul_left_of_ne_zero ha $
id       └──────────────────────────────┘ └┘
src      └──────────────────────────────┘
typ      └──────────────────────────────┘ └┘
doc      └──────────────────────────────┘
 74      calc
 75        2 * 2 * a * (a * x * x + b * x + c) = (2*a*x + b)^2 - (b^2 - 4*a*c) : by ring
id                                             
src                                                                └────
typ                                                   └────
doc                                                                                 └────
txt                                                                                 └────
par                                                                                 └────
pid                                                                                     
st                                                                                 └─────
 76        ... = 0 : by { rw [← h, discrim], ring }
id                                └─────┘
src  ─────┘               └────┘ └┘└─────┘  └───┘
typ  ─────┘               └────┘└┘└─────┘  └───┘
doc  ─────┘               └────┘ └┘└─────┘  └───┘
txt  ─────┘               └────┘ └┘         └───┘
par  ─────┘               └────┘ └┘         └───┘
pid  ─────┘                 └──┘ └┘             
st   ─────┘            └────────┘└───────┘└──────┘└┘
 77        ... = 2*2*a*0 : by ring)
id                 
src                        └──┘
typ                       └──┘
doc                           └──┘
txt                           └──┘
par                           └──┘
st                           └───┘
 78  
 79  /-- Roots of a quadratic -/
 80  lemma quadratic_eq_zero_iff (ha : a ≠ 0) {s : α} (h : discrim a b c = s * s) :
id                                                      └─────┘       
src                                                       └─────┘          
typ                                                     └─────┘       
doc                                                        └─────┘
 81    ∀ x : α, a * x * x + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a) := assume x,
id                                                                   
src                                                                   
typ                                                                  
 82  begin
st   └─────
 83    rw [quadratic_eq_zero_iff_discrim_eq_square ha, h, pow_two, mul_self_eq_mul_self_iff],
id         └─────────────────────────────────────┘ └┘    └─────┘  └──────────────────────┘
src    └──┘└─────────────────────────────────────┘  └┘ └┘└─────┘└┘└──────────────────────┘
typ    └──┘└─────────────────────────────────────┘└┘└┘└┘└─────┘└┘└──────────────────────┘
doc    └──┘└─────────────────────────────────────┘  └┘ └┘       └┘                        
txt    └──┘                                         └┘ └┘       └┘                        
par    └──┘                                         └┘ └┘       └┘                        
pid      └┘                                         └┘ └┘       └┘                        
st   ───────────────────────────────────────────────┘└─┘└───────┘└────────────────────────┘└──
 84    have ne : 2 * a ≠ 0 := mul_ne_zero two_ne_zero ha,
id                         └─────────┘ └─────────┘ └┘
src    └──────────┘ └────┘└─────────┘└─────────┘
typ    └──────────┘└────┘└─────────┘└─────────┘└┘
doc    └──────────┘   └────┘                      
txt    └──────────┘   └────┘                      
par    └──────────┘   └────┘                      
pid    └─────┘└───┘   └───┘                      
st   ──────────────────────────────────────────────────┘└─
 85    have : x = 2 * a * x / (2 * a) := (mul_div_cancel_left x ne).symm,
id                                    └─────────────────┘  └┘
src    └─────┘ └─┘     └┘  └───┘ └─────────────────┘ └┘└────┘
typ    └─────┘ └─┘    └┘ └───┘ └─────────────────┘└┘└────┘
doc    └─────┘  └─┘      └┘  └───┘                       └────┘
txt    └─────┘  └─┘      └┘  └───┘                       └────┘
par    └─────┘  └─┘      └┘  └───┘                       └────┘
pid    └───┘└┘  └─┘      └┘  └──┘                       └───┘
st   ──────────────────────────────────────────────────────────────────┘└─
 86    have h₁ : 2 * a * ((-b + s) / (2 * a)) = -b + s := mul_div_cancel' _ ne,
id                                                   └─────────────┘   └┘
src    └──────────┘       └┘  └┘  └─┘     └──┘└─────────────┘└─┘└┘
typ    └──────────┘       └┘  └┘ └─┘   └──┘└─────────────┘└─┘└┘
doc    └──────────┘         └┘  └┘  └─┘     └──┘               └─┘
txt    └──────────┘         └┘  └┘  └─┘     └──┘               └─┘
par    └──────────┘         └┘  └┘  └─┘     └──┘               └─┘
pid    └─────┘└───┘         └┘  └┘  └─┘     └──┘               └─┘
st   ────────────────────────────────────────────────────────────────────────┘└─
 87    have h₂ : 2 * a * ((-b - s) / (2 * a)) = -b - s := mul_div_cancel' _ ne,
id                                                    └─────────────┘   └┘
src    └──────────┘        └┘  └┘  └─┘     └──┘└─────────────┘└─┘└┘
typ    └──────────┘        └┘  └┘ └─┘   └──┘└─────────────┘└─┘└┘
doc    └──────────┘         └┘  └┘  └─┘     └──┘               └─┘
txt    └──────────┘         └┘  └┘  └─┘     └──┘               └─┘
par    └──────────┘         └┘  └┘  └─┘     └──┘               └─┘
pid    └─────┘└───┘         └┘  └┘  └─┘     └──┘               └─┘
st   ────────────────────────────────────────────────────────────────────────┘└─
 88    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
 89    { intro h', rcases h', { left, rw h', simpa }, { right, rw h', simpa } },
id                        └┘             └┘                       └┘
src      └──────┘  └─────┘      └──┘  └─┘    └────┘     └───┘  └─┘    └────┘
typ      └──────┘  └─────┘└┘    └──┘  └─┘└┘  └────┘     └───┘  └─┘└┘  └────┘
doc      └──────┘  └─────┘      └──┘  └─┘    └────┘     └───┘  └─┘    └────┘
txt      └──────┘  └─────┘      └──┘  └─┘    └────┘     └───┘  └─┘    └────┘
par      └──────┘  └─────┘      └──┘  └─┘    └────┘     └───┘  └─┘    └────┘
pid           └─┘                                                      
st   ───┘└──────┘└─────────┘└──┘└──┘└─────┘└──────┘└┘└──────┘└─────┘└──────┘└──┘
 90    { intro h', rcases h', { left, rw [h', h₁], ring }, { right, rw [h', h₂], ring } }
id                        └┘              └┘  └┘                        └┘  └┘
src      └──────┘  └─────┘      └──┘  └──┘  └┘    └───┘     └───┘  └──┘  └┘    └───┘
typ      └──────┘  └─────┘└┘    └──┘  └──┘└┘└┘└┘  └───┘     └───┘  └──┘└┘└┘└┘  └───┘
doc      └──────┘  └─────┘      └──┘  └──┘  └┘    └───┘     └───┘  └──┘  └┘    └───┘
txt      └──────┘  └─────┘      └──┘  └──┘  └┘    └───┘     └───┘  └──┘  └┘    └───┘
par      └──────┘  └─────┘      └──┘  └──┘  └┘    └───┘     └───┘  └──┘  └┘    └───┘
pid           └─┘                      └┘  └┘                      └┘  └┘        
st   ───────────┘└─────────┘└──┘└──┘└──────┘└──┘└──────┘└┘└──────┘└──────┘└──┘└──────┘└───
 91  end
st   ──┘
 92  
 93  /-- A quadratic has roots if its discriminant has square roots -/
 94  lemma exist_quadratic_eq_zero (ha : a ≠ 0) (h : ∃ s, discrim a b c = s * s) :
id                                                   └─────┘       
src                                                    └─────┘          
typ                                                  └─────┘       
doc                                                       └─────┘
 95    ∃ x, a * x * x + b * x + c = 0 :=
id                  
src                        
typ                 
 96  begin
st   └─────
 97    rcases h with ⟨s, hs⟩,
id            
src    └─────┘ └───────────┘
typ    └─────┘└───────────┘
doc    └─────┘ └───────────┘
txt    └─────┘ └───────────┘
par    └─────┘ └───────────┘
pid           └───────────┘
st   ──────────────────────┘└─
 98    use (-b + s) / (2 * a),
id                   
src    └──┘   └┘ └┘ 
typ    └──┘ └┘ └┘
doc    └──┘     └┘  └┘  
txt    └──┘     └┘  └┘  
par    └──┘     └┘  └┘  
pid            └┘  └┘  
st   ───────────────────────┘└─
 99    rw quadratic_eq_zero_iff ha hs,
id        └───────────────────┘ └┘ └┘
src    └─┘└───────────────────┘  
typ    └─┘└───────────────────┘└┘└┘
doc    └─┘└───────────────────┘  
txt    └─┘                       
par    └─┘                       
pid                             
st   ───────────────────────────────┘└─
100    simp
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
101  end
st   └─┘
102  
103  /-- Root of a quadratic when its discriminant equals zero -/
104  lemma quadratic_eq_zero_iff_of_discrim_eq_zero (ha : a ≠ 0) (h : discrim a b c = 0) :
id                                                                  └─────┘    
src                                                                  └─────┘       
typ                                                                 └─────┘    
doc                                                                   └─────┘
105    ∀ x : α, a * x * x + b * x + c = 0 ↔ x = -b / (2 * a) := assume x,
id                                                
src                                           
typ                                               
106  begin
st   └─────
107    have : discrim a b c = 0 * 0 := eq.trans h (by ring),
id            └─────┘             └──────┘ 
src    └─────┘└─────┘   └─┘└────┘└──────┘    └──┘
typ    └─────┘└─────┘└─┘└────┘└──────┘   └──┘
doc    └─────┘└─────┘    └─┘ └────┘            └──┘
txt    └─────┘           └─┘ └────┘            └──┘
par    └─────┘           └─┘ └────┘            └──┘
pid    └───┘└┘           └─┘ └───┘            └────┘
st   ───────────────────────────────────────────────┘└───┘└─
108    rw quadratic_eq_zero_iff ha this,
id        └───────────────────┘ └┘ └──┘
src    └─┘└───────────────────┘  
typ    └─┘└───────────────────┘└┘└──┘
doc    └─┘└───────────────────┘  
txt    └─┘                       
par    └─┘                       
pid                             
st   ─────────────────────────────────┘└─
109    simp
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
110  end
st   └─┘
111  
112  /-- A quadratic has no root if its discriminant has no square root. -/
113  lemma quadratic_ne_zero_of_discrim_ne_square (ha : a ≠ 0) (h : ∀ s : α, discrim a b c ≠ s * s) :
id                                                                        └─────┘       
src                                                                         └─────┘          
typ                                                                       └─────┘       
doc                                                                          └─────┘
114    ∀ (x : α), a * x * x + b * x + c ≠ 0 :=
id                          
src                                
typ                         
115  begin
st   └─────
116    assume x h',
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
117    rw [quadratic_eq_zero_iff_discrim_eq_square ha, pow_two] at h',
id         └─────────────────────────────────────┘ └┘  └─────┘
src    └──┘└─────────────────────────────────────┘  └┘└─────┘└─────┘
typ    └──┘└─────────────────────────────────────┘└┘└┘└─────┘└─────┘
doc    └──┘└─────────────────────────────────────┘  └┘       └─────┘
txt    └──┘                                         └┘       └─────┘
par    └──┘                                         └┘       └─────┘
pid      └┘                                         └┘       └────┘
st   ───────────────────────────────────────────────┘└───────┘└────┘└─
118    have := h _,
id             
src    └──────┘ └┘
typ    └──────┘└┘
doc    └──────┘ └┘
txt    └──────┘ └┘
par    └──────┘ └┘
pid    └───┘└─┘ └┘
st   ────────────┘└─
119    contradiction
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid                 
st   ───────────────┘
120  end
st   └─┘
121  
122  /-- If a polynomial of degree 2 is always nonnegative, then its discriminant is nonpositive -/
123  lemma discriminant_le_zero {a b c : α} (h : ∀ x : α,  0 ≤ a*x*x + b*x + c) : discrim a b c ≤ 0 :=
id                                                                  └─────┘    
src                                                                         └─────┘       
typ                                                                 └─────┘    
doc                                                                               └─────┘
124  have hc : 0 ≤ c, by { have := h 0, linarith },
id                               
src                       └──────┘ └┘  └───────┘
typ                      └──────┘└┘  └───────┘
doc                        └──────┘ └┘  └───────┘
txt                        └──────┘ └┘  └───────┘
par                        └──────┘ └┘  └───────┘
pid                        └───┘└─┘           
st                      └────────────┘└─────────┘└┘
125  begin
st   └─────
126    rw [discrim, pow_two],
id         └─────┘  └─────┘
src    └──┘└─────┘└┘└─────┘
typ    └──┘└─────┘└┘└─────┘
doc    └──┘└─────┘└┘       
txt    └──┘       └┘       
par    └──┘       └┘       
pid      └┘       └┘       
st   ────────────┘└───────┘└──
127    cases lt_trichotomy a 0 with ha ha,
id           └───────────┘ 
src    └────┘└───────────┘ └───────────┘
typ    └────┘└───────────┘└───────────┘
doc    └────┘              └───────────┘
txt    └────┘              └───────────┘
par    └────┘              └───────────┘
pid                       └──────────┘
st   ───────────────────────────────────┘└─
128    -- if a < 0
st   ──────────────
129    cases classical.em (b = 0) with hb hb,
id           └──────────┘  
src    └────┘└──────────┘   └────────────┘
typ    └────┘└──────────┘  └────────────┘
doc    └────┘               └────────────┘
txt    └────┘               └────────────┘
par    └────┘               └────────────┘
pid                        └─┘└─────────┘
st   ──────────────────────────────────────┘└─
130    { rw hb at *,
id          └┘
src      └─┘  └───┘
typ      └─┘└┘└───┘
doc      └─┘  └───┘
txt      └─┘  └───┘
par      └─┘  └───┘
pid          └───┘
st   ───┘└────────┘└─
131      rcases exists_lt_mul_self (-c/a) with ⟨x, hx⟩,
id              └────────────────┘   
src      └─────┘└────────────────┘    └────────────┘
typ      └─────┘└────────────────┘  └────────────┘
doc      └─────┘                       └────────────┘
txt      └─────┘                       └────────────┘
par      └─────┘                       └────────────┘
pid                                   └────────────┘
st   ────────────────────────────────────────────────┘└─
132      have := mul_lt_mul_of_neg_left hx ha,
id               └────────────────────┘ └┘ └┘
src      └──────┘└────────────────────┘  
typ      └──────┘└────────────────────┘└┘└┘
doc      └──────┘                        
txt      └──────┘                        
par      └──────┘                        
pid      └───┘└─┘                        
st   ───────────────────────────────────────┘└─
133      rw [mul_div_cancel' _ (ne_of_lt ha), ← mul_assoc] at this,
id           └─────────────┘    └──────┘ └┘     └───────┘
src      └──┘└─────────────┘└─┘ └──────┘  └───┘└───────┘└───────┘
typ      └──┘└─────────────┘└─┘ └──────┘└┘└───┘└───────┘└───────┘
doc      └──┘               └─┘           └───┘         └───────┘
txt      └──┘               └─┘           └───┘         └───────┘
par      └──┘               └─┘           └───┘         └───────┘
pid        └┘               └─┘           └───┘         └──────┘
st   ──────────────────────────────────────┘└───────────┘└──────┘└─
134      have h₂ := h x, linarith },
id                   
src      └─────────┘    └───────┘
typ      └─────────┘  └───────┘
doc      └─────────┘    └───────┘
txt      └─────────┘    └───────┘
par      └─────────┘    └───────┘
pid      └─────┘└─┘            
st   ─────────────────┘└─────────┘└┘
135    { cases classical.em (c = 0) with hc' hc',
id             └──────────┘  
src      └────┘└──────────┘   └──────────────┘
typ      └────┘└──────────┘  └──────────────┘
doc      └────┘               └──────────────┘
txt      └────┘               └──────────────┘
par      └────┘               └──────────────┘
pid                          └─┘└───────────┘
st   ───┘└─────────────────────────────────────┘└─
136      { rw hc' at *,
id            └─┘
src        └─┘   └───┘
typ        └─┘└─┘└───┘
doc        └─┘   └───┘
txt        └─┘   └───┘
par        └─┘   └───┘
pid             └───┘
st   ─────┘└─────────┘└─
137        have : -(a*-b*-b + b*-b + 0) = (1-a)*(b*b), ring,
id                                               
src        └─────┘               └──┘          └──┘
typ        └─────┘               └──┘        └──┘
doc        └─────┘               └──┘           └──┘
txt        └─────┘               └──┘           └──┘
par        └─────┘               └──┘           └──┘
pid        └───┘└┘               └──┘         
st   ───────────────────────────────────────────────┘└────┘└─
138        have h := h (-b), rw [← neg_nonpos, this] at h,
id                               └────────┘  └──┘
src        └────────┘      └────┘└────────┘└┘    └────┘
typ        └────────┘    └────┘└────────┘└┘└──┘└────┘
doc        └────────┘      └────┘          └┘    └────┘
txt        └────────┘      └────┘          └┘    └────┘
par        └────────┘      └────┘          └┘    └────┘
pid        └────┘└─┘        └──┘          └┘    └───┘
st   ─────────────────────┘└────────────────┘└────┘└───┘└─
139        have : b * b ≤ 0, from nonpos_of_mul_nonpos_left h (by linarith),
id                              └───────────────────────┘ 
src        └─────┘   └┘  └───┘└───────────────────────┘    └──────┘
typ        └─────┘  └┘  └───┘└───────────────────────┘   └──────┘
doc        └─────┘    └┘  └───┘                             └──────┘
txt        └─────┘    └┘  └───┘                             └──────┘
par        └─────┘    └┘  └───┘                             └──────┘
pid        └───┘└┘      └───┘                             └────────┘
st   ─────────────────────┘└────────────────────────────────────┘└───────┘└─
140        linarith },
src        └───────┘
typ        └───────┘
doc        └───────┘
txt        └───────┘
par        └───────┘
pid                
st   ──────────────┘└┘
141      { have h := h (-c/b),
id                       
src        └────────┘      
typ        └────────┘   
doc        └────────┘      
txt        └────────┘      
par        └────────┘      
pid        └────┘└─┘      
st   ───────────────────────┘└─
142        have : a*(-c/b)*(-c/b) + b*(-c/b) + c = a*((c/b)*(c/b)),
id                                                           
src        └─────┘             └┘        └┘               └┘
typ        └─────┘             └┘        └┘            └┘
doc        └─────┘             └┘        └┘               └┘
txt        └─────┘             └┘        └┘               └┘
par        └─────┘             └┘        └┘               └┘
pid        └───┘└┘             └┘        └┘               └┘
st   ────────────────────────────────────────────────────────────┘└─
143          rw mul_div_cancel' _ hb, ring,
id              └─────────────┘   └┘
src          └─┘└─────────────┘└─┘    └──┘
typ          └─┘└─────────────┘└─┘└┘  └──┘
doc          └─┘               └─┘    └──┘
txt          └─┘               └─┘    └──┘
par          └─┘               └─┘    └──┘
pid                           └─┘
st   ──────────────────────────────┘└────┘└─
144        rw this at h,
id            └──┘
src        └─┘    └───┘
typ        └─┘└──┘└───┘
doc        └─┘    └───┘
txt        └─┘    └───┘
par        └─┘    └───┘
pid              └───┘
st   ─────────────────┘└─
145        have : 0 ≤ a := nonneg_of_mul_nonneg_right h (mul_self_pos $ div_ne_zero hc' hb),
id                        └────────────────────────┘   └──────────┘   └─────────┘ └─┘ └┘
src        └───────┘  └──┘└────────────────────────┘  └──────────┘ └─────────┘     
typ        └───────┘ └──┘└────────────────────────┘ └──────────┘ └─────────┘└─┘└┘
doc        └───────┘  └──┘                                                         
txt        └───────┘  └──┘                                                         
par        └───────┘  └──┘                                                         
pid        └───┘└──┘  └──┘                                                         
st   ─────────────────────────────────────────────────────────────────────────────────────┘└─
146        linarith [ha] } },
id                   └┘
src        └────────┘  └┘
typ        └────────┘└┘└┘
doc        └────────┘  └┘
txt        └────────┘  └┘
par        └────────┘  └┘
pid                  
st   ───────────────────┘└──┘
147    cases ha with ha ha,
id           └┘
src    └────┘  └─────────┘
typ    └────┘└┘└─────────┘
doc    └────┘  └─────────┘
txt    └────┘  └─────────┘
par    └────┘  └─────────┘
pid           └─────────┘
st   ────────────────────┘└─
148    -- if a = 0
st   ──────────────
149    cases classical.em (b = 0) with hb hb,
id           └──────────┘  
src    └────┘└──────────┘   └────────────┘
typ    └────┘└──────────┘  └────────────┘
doc    └────┘               └────────────┘
txt    └────┘               └────────────┘
par    └────┘               └────────────┘
pid                        └─┘└─────────┘
st   ──────────────────────────────────────┘└─
150      { rw [ha, hb], linarith },
id             └┘  └┘
src        └──┘  └┘    └───────┘
typ        └──┘└┘└┘└┘  └───────┘
doc        └──┘  └┘    └───────┘
txt        └──┘  └┘    └───────┘
par        └──┘  └┘    └───────┘
pid          └┘  └┘            
st   ─────┘└────┘└──┘└─────────┘└┘
151      { have := h ((-c-1)/b), rw [ha, mul_div_cancel' _ hb] at this, linarith },
id                                └┘  └─────────────┘   └┘
src        └──────┘      └┘    └──┘  └┘└─────────────┘└─┘  └───────┘  └───────┘
typ        └──────┘    └┘   └──┘└┘└┘└─────────────┘└─┘└┘└───────┘  └───────┘
doc        └──────┘      └┘    └──┘  └┘               └─┘  └───────┘  └───────┘
txt        └──────┘      └┘    └──┘  └┘               └─┘  └───────┘  └───────┘
par        └──────┘      └┘    └──┘  └┘               └─┘  └───────┘  └───────┘
pid        └───┘└─┘      └┘      └┘  └┘               └─┘  └──────┘          
st   ─────┘└──────────────────┘└──────┘└────────────────────┘└──────┘└─────────┘└┘
152    -- if a > 0
st   ──────────────
153    have := calc
src    └──────┘    
typ    └──────┘    
doc    └──────┘    
txt    └──────┘    
par    └──────┘    
pid    └───┘└─┘    
st   ───────────────
154      4*a* (a*(-(b/a)*(1/2))*(-(b/a)*(1/2)) + b*(-(b/a)*(1/2)) + c)
src  ────┘               └─┘          └──┘            └──┘  └─
typ  ────┘               └─┘          └──┘            └──┘  └─
doc  ────┘               └─┘          └──┘            └──┘  └─
txt  ────┘               └─┘          └──┘            └──┘  └─
par  ────┘               └─┘          └──┘            └──┘  └─
pid  ────┘               └─┘          └──┘            └──┘  └─
st   ──────────────────────────────────────────────────────────────────
155        = (a*(b/a)) * (a*(b/a)) - 2*(a*(b/a))*b + 4*a*c : by ring
src  ─────┘        └─┘        └─┘ └┘        └┘   └┘    └─┘  └────
typ  ─────┘        └─┘        └─┘ └┘        └┘   └┘    └─┘  └────
doc  ─────┘        └─┘        └─┘ └┘        └┘   └┘    └─┘  └────
txt  ─────┘        └─┘        └─┘ └┘        └┘   └┘    └─┘  └────
par  ─────┘        └─┘        └─┘ └┘        └┘   └┘    └─┘  └────
pid  ─────┘        └─┘        └─┘ └┘        └┘   └┘    └─┘  └─────
st   ─────────────────────────────────────────────────────────┘└─────
156      ... = -(b*b - 4*a*c) : by { simp only [mul_div_cancel' b (ne_of_gt ha)], ring },
id                                           └─────────────┘   └──────┘ └┘
src  ───┘└──┘       └┘    └──┘  └─┘└─────────┘└─────────────┘  └──────┘  └┘└┘└───┘
typ  ───┘└──┘      └┘  └──┘  └─┘└─────────┘└─────────────┘ └──────┘└┘└┘└┘└───┘
doc  ───┘└──┘       └┘    └──┘  └─┘└─────────┘                           └┘└┘└───┘
txt  ───┘└──┘       └┘    └──┘  └─┘└─────────┘                           └┘└┘└───┘
par  ───┘└──┘       └┘    └──┘  └─┘└─────────┘                           └┘└┘└───┘
pid  ───────┘       └┘    └──┘  └────────────┘                           └────────┘
st   ───┘└───────────────────────┘└────────────────────────────────────────────┘└─────┘└┘
157    have ha' : 0 ≤ 4*a, linarith,
id                      
src    └───────────┘ └┘    └──────┘
typ    └───────────┘ └┘   └──────┘
doc    └───────────┘ └┘    └──────┘
txt    └───────────┘ └┘    └──────┘
par    └───────────┘ └┘    └──────┘
pid    └──────┘└───┘ └┘
st   ───────────────────┘└────────┘└─
158    have h := (mul_nonneg ha' (h (-(b/a) * (1/2)))),
id                └────────┘ └─┘       
src    └────────┘ └────────┘           └┘   └───┘
typ    └────────┘ └────────┘└─┘     └┘   └───┘
doc    └────────┘                      └┘   └───┘
txt    └────────┘                      └┘   └───┘
par    └────────┘                      └┘   └───┘
pid    └────┘└─┘                      └┘   └───┘
st   ────────────────────────────────────────────────┘└─
159    rw this at h, rwa ← neg_nonneg
id        └──┘             └────────┘
src    └─┘    └───┘  └────┘└────────┘
typ    └─┘└──┘└───┘  └────┘└────────┘
doc    └─┘    └───┘  └────┘          
txt    └─┘    └───┘  └────┘          
par    └─┘    └───┘  └────┘          
pid          └───┘     └─┘          
st   ─────────────┘└─────────────────┘
160  end
st   └─┘
161  
162  /--
163  If a polynomial of degree 2 is always positive, then its discriminant is negative,
164  at least when the coefficient of the quadratic term is nonzero.
165  -/
166  lemma discriminant_lt_zero {a b c : α} (ha : a ≠ 0) (h : ∀ x : α,  0 < a*x*x + b*x + c) :
id                                                                         
src                                                                               
typ                                                                        
167    discrim a b c < 0 :=
id     └─────┘    
src    └─────┘       
typ    └─────┘    
doc    └─────┘
168  begin
st   └─────
169    have : ∀ x : α,  0 ≤ a*x*x + b*x + c := assume x, le_of_lt (h x),
id                                                └──────┘  
src    └─────┘ └───┘  └──┘         └──┘      └──┘└──────┘   
typ    └─────┘ └───┘ └──┘      └──┘      └──┘└──────┘  
doc    └─────┘ └───┘  └──┘            └──┘      └──┘           
txt    └─────┘ └───┘  └──┘            └──┘      └──┘           
par    └─────┘ └───┘  └──┘            └──┘      └──┘           
pid    └───┘└┘ └───┘  └──┘            └──┘      └──┘           
st   ─────────────────────────────────────────────────────────────────┘└─
170    refine lt_of_le_of_ne (discriminant_le_zero this) _,
id            └────────────┘  └──────────────────┘ └──┘
src    └─────┘└────────────┘ └──────────────────┘    └─┘
typ    └─────┘└────────────┘ └──────────────────┘└──┘└─┘
doc    └─────┘               └──────────────────┘    └─┘
txt    └─────┘                                       └─┘
par    └─────┘                                       └─┘
pid                                                 └─┘
st   ────────────────────────────────────────────────────┘└─
171    assume h',
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid    └───────┘
st   ──────────┘└─
172    have := h (-b / (2 * a)),
id                      
src    └──────┘    └┘  └┘
typ    └──────┘  └┘ └┘
doc    └──────┘      └┘  └┘
txt    └──────┘      └┘  └┘
par    └──────┘      └┘  └┘
pid    └───┘└─┘      └┘  └┘
st   ─────────────────────────┘└─
173    have : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0,
id                                                                      
src    └─────┘       └┘  └─┘      └┘  └─┘        └┘  └─┘  └┘
typ    └─────┘       └┘  └─┘      └┘  └─┘       └┘ └─┘ └┘
doc    └─────┘       └┘  └─┘      └┘  └─┘        └┘  └─┘   └┘
txt    └─────┘       └┘  └─┘      └┘  └─┘        └┘  └─┘   └┘
par    └─────┘       └┘  └─┘      └┘  └─┘        └┘  └─┘   └┘
pid    └───┘└┘       └┘  └─┘      └┘  └─┘        └┘  └─┘   
st   ────────────────────────────────────────────────────────────────────────┘└─
174      rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))],
id           └──────────────────────────────────────┘ └┘ └┘           
src      └──┘└──────────────────────────────────────┘         └┘  └─┘
typ      └──┘└──────────────────────────────────────┘└┘└┘    └┘ └─┘
doc      └──┘└──────────────────────────────────────┘         └┘  └─┘
txt      └──┘                                                 └┘  └─┘
par      └──┘                                                 └┘  └─┘
pid        └┘                                                 └┘  └─┘
st   ────────────────────────────────────────────────────────────────────┘└──
175    linarith
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid            
st   ──────────┘
176  end
st   └─┘